PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 16:06:49 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 consensus.6.prism consensus.props --property steps_min -const K=2
Parsing model file "consensus.6.prism"...
Type: MDP
Modules: process1 process2 process3 process4 process5 process6
Variables: counter pc1 coin1 pc2 coin2 pc3 coin3 pc4 coin4 pc5 coin5 pc6 coin6
Parsing properties file "consensus.props"...
5 properties:
(1) "c1": P>=1 [ F "finished" ]
(2) "c2": Pmin=? [ F "finished"&"all_coins_equal_1" ]
(3) "disagree": Pmax=? [ F "finished"&!"agree" ]
(4) "steps_max": R{"steps"}max=? [ F "finished" ]
(5) "steps_min": R{"steps"}min=? [ F "finished" ]
---------------------------------------------------------------------
Model checking: "steps_min": R{"steps"}min=? [ F "finished" ]
Model constants: K=2
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Warning: Switching to explicit engine to allow interval iteration on Rmin operator.
Building model...
Model constants: K=2
Computing reachable states... 197054 451271 702566 996506 1258240 states
Reachable states exploration and model construction done in 14.303 secs.
Sorting reachable states list...
Time for model construction: 17.963 seconds.
Type: MDP
States: 1258240 (1 initial)
Transitions: 6236736
Choices: 5008128
Max/avg: 6/3.98
Building reward structure...
Starting expected reachability (min)...
Starting Prob1 (max)...
Prob1 (max) took 49 iterations and 3.531 seconds.
target=384, inf=0, rest=1257856
For Rmin, checking for zero-reward ECs...
Time for checking for zero-reward ECs: 0.256 seconds, no zero-reward ECs found, proceeding normally.
Computing upper bound(s) for Rmin using the Dijkstra Sweep for Monotone Pessimistic Initialization algorithm...
Calculating incoming choices relation for Markov decision process... done (0.553 seconds)
Time for computing upper bound(s) for Rmin using the DSI-MP algorithm: 7.023 seconds.
Upper bound for min expectation (Dijkstra Sweep MPI): 18438.0
Starting Prob1 (min)...
Prob1 (min) took 64 iterations and 4.394 seconds.
Relevant sub-MDP is contracting, proceed...
Starting interval iteration (min, with Power method)...
Iteration 32: max relative diff=575.1875, 5.14 sec so far
Iteration 65: max relative diff=281.858085095, 10.20 sec so far
Iteration 98: max relative diff=180.475874072, 15.22 sec so far
Iteration 131: max relative diff=128.815196069, 20.25 sec so far
Iteration 164: max relative diff=96.7438860208, 25.27 sec so far
Iteration 197: max relative diff=76.231789396, 30.30 sec so far
Iteration 230: max relative diff=61.3128913528, 35.34 sec so far
Iteration 263: max relative diff=50.735766537, 40.37 sec so far
Iteration 296: max relative diff=42.3810409556, 45.41 sec so far
Iteration 329: max relative diff=36.0788808003, 50.44 sec so far
Iteration 362: max relative diff=30.8450528979, 55.47 sec so far
Iteration 394: max relative diff=26.8260847707, 60.57 sec so far
Iteration 427: max relative diff=23.2867983469, 65.62 sec so far
Iteration 460: max relative diff=20.4259914999, 70.66 sec so far
Iteration 493: max relative diff=17.92061122, 75.69 sec so far
Iteration 526: max relative diff=15.8557182442, 80.72 sec so far
Iteration 559: max relative diff=14.0180397398, 85.75 sec so far
Iteration 592: max relative diff=12.4817912232, 90.77 sec so far
Iteration 625: max relative diff=11.0982704443, 95.81 sec so far
Iteration 658: max relative diff=9.9293115258, 100.87 sec so far
Iteration 691: max relative diff=8.86708987149, 105.89 sec so far
Iteration 724: max relative diff=7.96226742047, 110.92 sec so far
Iteration 757: max relative diff=7.13437509325, 115.95 sec so far
Iteration 790: max relative diff=6.42468491373, 120.98 sec so far
Iteration 823: max relative diff=5.77182949262, 126.05 sec so far
Iteration 856: max relative diff=5.20939357313, 131.08 sec so far
Iteration 889: max relative diff=4.68979618695, 136.11 sec so far
Iteration 922: max relative diff=4.24038901647, 141.14 sec so far
Iteration 955: max relative diff=3.82380346162, 146.17 sec so far
Iteration 988: max relative diff=3.46235031355, 151.20 sec so far
Iteration 1021: max relative diff=3.12638389992, 156.25 sec so far
Iteration 1054: max relative diff=2.83413611393, 161.28 sec so far
Iteration 1087: max relative diff=2.56189923227, 166.31 sec so far
Iteration 1120: max relative diff=2.32459850953, 171.36 sec so far
Iteration 1153: max relative diff=2.10315322001, 176.41 sec so far
Iteration 1186: max relative diff=1.90980173988, 181.44 sec so far
Iteration 1219: max relative diff=1.72910813203, 186.48 sec so far
Iteration 1252: max relative diff=1.57112222646, 191.50 sec so far
Iteration 1285: max relative diff=1.42330463338, 196.54 sec so far
Iteration 1318: max relative diff=1.29391847653, 201.56 sec so far
Iteration 1351: max relative diff=1.1727429437, 206.58 sec so far
Iteration 1384: max relative diff=1.06657949822, 211.61 sec so far
Iteration 1417: max relative diff=0.967074257833, 216.68 sec so far
Iteration 1450: max relative diff=0.879830760447, 221.71 sec so far
Iteration 1483: max relative diff=0.798005689079, 226.74 sec so far
Iteration 1516: max relative diff=0.726219254425, 231.76 sec so far
Iteration 1549: max relative diff=0.658855242874, 236.79 sec so far
Iteration 1582: max relative diff=0.599725600603, 241.82 sec so far
Iteration 1615: max relative diff=0.544214221538, 246.87 sec so far
Iteration 1648: max relative diff=0.495467919251, 251.90 sec so far
Iteration 1681: max relative diff=0.449687894871, 256.92 sec so far
Iteration 1714: max relative diff=0.409473082558, 261.95 sec so far
Iteration 1747: max relative diff=0.371694091941, 266.97 sec so far
Iteration 1780: max relative diff=0.338498191714, 272.00 sec so far
Iteration 1813: max relative diff=0.307305273354, 277.05 sec so far
Iteration 1846: max relative diff=0.279890002277, 282.09 sec so far
Iteration 1879: max relative diff=0.254123666478, 287.11 sec so far
Iteration 1912: max relative diff=0.23147337435, 292.16 sec so far
Iteration 1945: max relative diff=0.210181834015, 297.19 sec so far
Iteration 1978: max relative diff=0.191462166182, 302.23 sec so far
Iteration 2011: max relative diff=0.173863009204, 307.26 sec so far
Iteration 2044: max relative diff=0.158387651135, 312.29 sec so far
Iteration 2077: max relative diff=0.143836933813, 317.31 sec so far
Iteration 2110: max relative diff=0.131040733825, 322.33 sec so far
Iteration 2143: max relative diff=0.119007952292, 327.35 sec so far
Iteration 2176: max relative diff=0.108425114186, 332.40 sec so far
Iteration 2209: max relative diff=0.0984728629265, 337.44 sec so far
Iteration 2242: max relative diff=0.0897191938082, 342.47 sec so far
Iteration 2275: max relative diff=0.081486583367, 347.49 sec so far
Iteration 2308: max relative diff=0.0742450024485, 352.52 sec so far
Iteration 2341: max relative diff=0.0674341071571, 357.54 sec so far
Iteration 2374: max relative diff=0.0614427889549, 362.56 sec so far
Iteration 2407: max relative diff=0.0558075473393, 367.67 sec so far
Iteration 2440: max relative diff=0.0508502014318, 372.69 sec so far
Iteration 2473: max relative diff=0.0461873091694, 377.71 sec so far
Iteration 2506: max relative diff=0.0420851985195, 382.74 sec so far
Iteration 2539: max relative diff=0.0382266250934, 387.76 sec so far
Iteration 2572: max relative diff=0.03483200306, 392.79 sec so far
Iteration 2605: max relative diff=0.0316388349684, 397.81 sec so far
Iteration 2638: max relative diff=0.0288295427246, 402.84 sec so far
Iteration 2671: max relative diff=0.026186912836, 407.89 sec so far
Iteration 2704: max relative diff=0.0238619278264, 412.92 sec so far
Iteration 2737: max relative diff=0.0216748356668, 417.95 sec so far
Iteration 2770: max relative diff=0.0197506008082, 423.00 sec so far
Iteration 2803: max relative diff=0.0179404647692, 428.05 sec so far
Iteration 2836: max relative diff=0.0163478594884, 433.07 sec so far
Iteration 2869: max relative diff=0.014849671093, 438.09 sec so far
Iteration 2902: max relative diff=0.0135315106237, 443.12 sec so far
Iteration 2935: max relative diff=0.0122914845557, 448.15 sec so far
Iteration 2968: max relative diff=0.0112004544359, 453.18 sec so far
Iteration 3001: max relative diff=0.0101740871686, 458.22 sec so far
Iteration 3034: max relative diff=0.00927103656415, 463.25 sec so far
Iteration 3067: max relative diff=0.0084215019963, 468.27 sec so far
Iteration 3100: max relative diff=0.00767403307784, 473.29 sec so far
Iteration 3133: max relative diff=0.00697085630258, 478.31 sec so far
Iteration 3166: max relative diff=0.00635215802092, 483.35 sec so far
Iteration 3199: max relative diff=0.005770118752, 488.38 sec so far
Iteration 3232: max relative diff=0.0052580024642, 493.41 sec so far
Iteration 3265: max relative diff=0.00477622817618, 498.43 sec so far
Iteration 3298: max relative diff=0.00435233004495, 503.45 sec so far
Iteration 3331: max relative diff=0.00395354588487, 508.48 sec so far
Iteration 3364: max relative diff=0.00360266711451, 513.50 sec so far
Iteration 3397: max relative diff=0.00327257540078, 518.52 sec so far
Iteration 3430: max relative diff=0.00298213642352, 523.58 sec so far
Iteration 3463: max relative diff=0.00270890328787, 528.60 sec so far
Iteration 3496: max relative diff=0.00246849217463, 533.63 sec so far
Iteration 3529: max relative diff=0.00224232280751, 538.65 sec so far
Iteration 3562: max relative diff=0.00204332160602, 543.68 sec so far
Iteration 3595: max relative diff=0.00185610878648, 548.72 sec so far
Iteration 3628: max relative diff=0.0016913843182, 553.74 sec so far
Iteration 3661: max relative diff=0.00153641756587, 558.78 sec so far
Iteration 3694: max relative diff=0.00140006554765, 563.81 sec so far
Iteration 3727: max relative diff=0.0012717904282, 568.84 sec so far
Iteration 3760: max relative diff=0.00115892371246, 573.86 sec so far
Iteration 3793: max relative diff=0.00105274263955, 578.89 sec so far
Iteration 3826: max relative diff=0.000959315959137, 583.92 sec so far
Iteration 3859: max relative diff=0.000871423332981, 588.94 sec so far
Iteration 3892: max relative diff=0.000794088253146, 593.97 sec so far
Iteration 3925: max relative diff=0.000721334012743, 599.02 sec so far
Iteration 3958: max relative diff=0.000657318880528, 604.07 sec so far
Iteration 3991: max relative diff=0.000597095569916, 609.10 sec so far
Iteration 4024: max relative diff=0.000544106150676, 614.13 sec so far
Iteration 4057: max relative diff=0.000494255445066, 619.15 sec so far
Iteration 4090: max relative diff=0.000450392679843, 624.18 sec so far
Iteration 4123: max relative diff=0.00040912801719, 629.21 sec so far
Iteration 4156: max relative diff=0.000372819949886, 634.28 sec so far
Iteration 4189: max relative diff=0.000338662492061, 639.30 sec so far
Iteration 4222: max relative diff=0.000308607924349, 644.34 sec so far
Iteration 4255: max relative diff=0.000280333550785, 649.36 sec so far
Iteration 4288: max relative diff=0.000255455403799, 654.39 sec so far
Iteration 4321: max relative diff=0.000232050836539, 659.41 sec so far
Iteration 4354: max relative diff=0.000211457546784, 664.43 sec so far
Iteration 4387: max relative diff=0.000192084033588, 669.47 sec so far
Iteration 4420: max relative diff=0.000175037598813, 674.49 sec so far
Iteration 4453: max relative diff=0.000159000852142, 679.52 sec so far
Iteration 4486: max relative diff=0.000144890381496, 684.54 sec so far
Iteration 4519: max relative diff=0.000131615695625, 689.58 sec so far
Iteration 4552: max relative diff=0.000119935515849, 694.60 sec so far
Iteration 4585: max relative diff=0.000108947170046, 699.62 sec so far
Iteration 4618: max relative diff=9.92787028368e-05, 704.64 sec so far
Iteration 4651: max relative diff=9.01829122954e-05, 709.68 sec so far
Iteration 4684: max relative diff=8.2179673208e-05, 714.70 sec so far
Iteration 4717: max relative diff=7.46504765789e-05, 719.73 sec so far
Iteration 4750: max relative diff=6.80256577779e-05, 724.76 sec so far
Iteration 4783: max relative diff=6.17932354678e-05, 729.79 sec so far
Iteration 4816: max relative diff=5.63094272381e-05, 734.82 sec so far
Iteration 4849: max relative diff=5.11504317732e-05, 739.84 sec so far
Iteration 4882: max relative diff=4.66111143961e-05, 744.90 sec so far
Iteration 4915: max relative diff=4.23406662758e-05, 749.92 sec so far
Iteration 4948: max relative diff=3.85831673362e-05, 754.95 sec so far
Iteration 4981: max relative diff=3.50482295032e-05, 759.98 sec so far
Iteration 5014: max relative diff=3.19378942083e-05, 765.00 sec so far
Iteration 5047: max relative diff=2.90117876846e-05, 770.02 sec so far
Iteration 5080: max relative diff=2.64371532696e-05, 775.05 sec so far
Iteration 5113: max relative diff=2.40150173944e-05, 780.08 sec so far
Iteration 5146: max relative diff=2.18838186682e-05, 785.10 sec so far
Iteration 5179: max relative diff=1.98788532469e-05, 790.14 sec so far
Iteration 5212: max relative diff=1.81147161231e-05, 795.17 sec so far
Iteration 5245: max relative diff=1.64550708098e-05, 800.19 sec so far
Iteration 5278: max relative diff=1.49947753276e-05, 805.22 sec so far
Iteration 5311: max relative diff=1.36209747616e-05, 810.24 sec so far
Iteration 5344: max relative diff=1.24121895082e-05, 815.27 sec so far
Iteration 5377: max relative diff=1.12750019317e-05, 820.31 sec so far
Iteration 5410: max relative diff=1.02744086734e-05, 825.33 sec so far
Iteration 5443: max relative diff=9.33308164456e-06, 830.36 sec so far
Iteration 5476: max relative diff=8.50482296043e-06, 835.39 sec so far
Iteration 5509: max relative diff=7.72562293673e-06, 840.41 sec so far
Iteration 5542: max relative diff=7.04001722172e-06, 845.49 sec so far
Iteration 5575: max relative diff=6.39502067411e-06, 850.51 sec so far
Iteration 5608: max relative diff=5.82749846165e-06, 855.56 sec so far
Iteration 5641: max relative diff=5.29359120098e-06, 860.59 sec so far
Iteration 5674: max relative diff=4.82381468461e-06, 865.62 sec so far
Iteration 5707: max relative diff=4.38186353586e-06, 870.64 sec so far
Iteration 5740: max relative diff=3.99299774018e-06, 875.67 sec so far
Iteration 5773: max relative diff=3.62716488213e-06, 880.69 sec so far
Iteration 5806: max relative diff=3.3052743602e-06, 885.72 sec so far
Iteration 5839: max relative diff=3.00244975803e-06, 890.75 sec so far
Iteration 5872: max relative diff=2.7359991993e-06, 895.77 sec so far
Iteration 5905: max relative diff=2.48533079212e-06, 900.79 sec so far
Iteration 5938: max relative diff=2.26477164011e-06, 905.82 sec so far
Iteration 5971: max relative diff=2.05727644206e-06, 910.84 sec so far
Iteration 6004: max relative diff=1.8747047116e-06, 915.87 sec so far
Iteration 6037: max relative diff=1.70294689915e-06, 920.90 sec so far
Iteration 6070: max relative diff=1.55181992644e-06, 925.92 sec so far
Iteration 6103: max relative diff=1.40964436486e-06, 930.96 sec so far
Iteration 6136: max relative diff=1.28454634562e-06, 935.98 sec so far
Iteration 6169: max relative diff=1.16685801466e-06, 941.01 sec so far
Iteration 6202: max relative diff=1.06330592053e-06, 946.04 sec so far
Max relative diff between upper and lower bound on convergence: 9.9965974348e-07
Interval iteration (min, with Power method) took 6223 iterations, 77617636992 multiplications and 949.42 seconds.
Maximum finite value in solution vector at end of interval iteration: 444.00021153300156
Expected reachability took 964.74 seconds.
Value in the initial state: 432.0002043865894
Time for model checking: 965.479 seconds.
Result: 432.0002043865894 (value in the initial state)
Overall running time: 984.047 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.